$\forall$${\it es}$:ES, $e$, ${\it e'}$:E. $\neg$first($e$) $\Rightarrow$ pred($e$) $\leq$ ${\it e'}$  $\Rightarrow$ (${\it e'}$ $<$loc $e$) $\Rightarrow$ ${\it e'}$ $=$ pred($e$)